YES 1.988
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule List
|
| ((delete :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | delete :: Eq a => a -> [a] -> [a]
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | if x `eq` y then ys else y : deleteBy eq x ys |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys
is transformed to
| deleteBy0 | ys y eq x True | = ys |
| deleteBy0 | ys y eq x False | = y : deleteBy eq x ys |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
|
| ((delete :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | delete :: Eq a => a -> [a] -> [a]
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
|
| ((delete :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | delete :: Eq a => a -> [a] -> [a]
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
|
| (delete :: Eq a => Maybe a -> [Maybe a] -> [Maybe a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | delete :: Eq a => a -> [a] -> [a]
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy2000), Succ(xy4001000)) → new_primPlusNat(xy2000, xy4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy2000), Succ(xy4001000)) → new_primPlusNat(xy2000, xy4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy30100), Succ(xy400100)) → new_primMulNat(xy30100, Succ(xy400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy30100), Succ(xy400100)) → new_primMulNat(xy30100, Succ(xy400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy3000), Succ(xy40000)) → new_primEqNat(xy3000, xy40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy3000), Succ(xy40000)) → new_primEqNat(xy3000, xy40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(ty_@2, bce), bcf), bah) → new_esEs1(xy301, xy4001, bce, bcf)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(ty_Maybe, bcg), bah) → new_esEs2(xy301, xy4001, bcg)
new_esEs0(Left(xy300), Left(xy4000), app(ty_[], cc), cd) → new_esEs(xy300, xy4000, cc)
new_esEs2(Just(xy300), Just(xy4000), app(ty_[], he)) → new_esEs(xy300, xy4000, he)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xy301, xy4001, hb, hc, hd)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(app(ty_@3, bea), beb), bec)) → new_esEs3(xy302, xy4002, bea, beb, bec)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(ty_[], bdc)) → new_esEs(xy302, xy4002, bdc)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_Either, fb), fc), fa) → new_esEs0(xy300, xy4000, fb, fc)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_Either, ge), gf)) → new_esEs0(xy301, xy4001, ge, gf)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bbc), bbd), bag, bah) → new_esEs1(xy300, xy4000, bbc, bbd)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xy300, xy4000, bg, bh, ca)
new_esEs0(Right(xy300), Right(xy4000), df, app(app(ty_@2, eb), ec)) → new_esEs1(xy300, xy4000, eb, ec)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_[], baf), bag, bah) → new_esEs(xy300, xy4000, baf)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(ty_[], bcb), bah) → new_esEs(xy301, xy4001, bcb)
new_esEs0(Left(xy300), Left(xy4000), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xy300, xy4000, dc, dd, de)
new_esEs2(Just(xy300), Just(xy4000), app(ty_Maybe, bab)) → new_esEs2(xy300, xy4000, bab)
new_esEs0(Left(xy300), Left(xy4000), app(app(ty_Either, ce), cf), cd) → new_esEs0(xy300, xy4000, ce, cf)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_@2, hh), baa)) → new_esEs1(xy300, xy4000, hh, baa)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_[], gd)) → new_esEs(xy301, xy4001, gd)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_Maybe, bf)) → new_esEs2(xy300, xy4000, bf)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_Maybe, fg), fa) → new_esEs2(xy300, xy4000, fg)
new_esEs0(Right(xy300), Right(xy4000), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xy300, xy4000, ee, ef, eg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_[], eh), fa) → new_esEs(xy300, xy4000, eh)
new_esEs0(Right(xy300), Right(xy4000), df, app(app(ty_Either, dh), ea)) → new_esEs0(xy300, xy4000, dh, ea)
new_esEs0(Left(xy300), Left(xy4000), app(ty_Maybe, db), cd) → new_esEs2(xy300, xy4000, db)
new_esEs0(Right(xy300), Right(xy4000), df, app(ty_Maybe, ed)) → new_esEs2(xy300, xy4000, ed)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_@2, gg), gh)) → new_esEs1(xy301, xy4001, gg, gh)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_@2, bd), be)) → new_esEs1(xy300, xy4000, bd, be)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(app(ty_@3, bch), bda), bdb), bah) → new_esEs3(xy301, xy4001, bch, bda, bdb)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_Either, bb), bc)) → new_esEs0(xy300, xy4000, bb, bc)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), cb) → new_esEs(xy301, xy4001, cb)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(ty_@2, bdf), bdg)) → new_esEs1(xy302, xy4002, bdf, bdg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(app(ty_@3, fh), ga), gb), fa) → new_esEs3(xy300, xy4000, fh, ga, gb)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_@2, fd), ff), fa) → new_esEs1(xy300, xy4000, fd, ff)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bbe), bag, bah) → new_esEs2(xy300, xy4000, bbe)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(ty_Maybe, bdh)) → new_esEs2(xy302, xy4002, bdh)
new_esEs0(Right(xy300), Right(xy4000), df, app(ty_[], dg)) → new_esEs(xy300, xy4000, dg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_Maybe, ha)) → new_esEs2(xy301, xy4001, ha)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_Either, hf), hg)) → new_esEs0(xy300, xy4000, hf, hg)
new_esEs2(Just(xy300), Just(xy4000), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy300, xy4000, bac, bad, bae)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(ty_Either, bcc), bcd), bah) → new_esEs0(xy301, xy4001, bcc, bcd)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(ty_Either, bdd), bde)) → new_esEs0(xy302, xy4002, bdd, bde)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_[], ba)) → new_esEs(xy300, xy4000, ba)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bbf), bbg), bbh), bag, bah) → new_esEs3(xy300, xy4000, bbf, bbg, bbh)
new_esEs0(Left(xy300), Left(xy4000), app(app(ty_@2, cg), da), cd) → new_esEs1(xy300, xy4000, cg, da)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bba), bbb), bag, bah) → new_esEs0(xy300, xy4000, bba, bbb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(xy300), Just(xy4000), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xy300, xy4000, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(xy300), Just(xy4000), app(app(ty_Either, hf), hg)) → new_esEs0(xy300, xy4000, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xy300, xy4000, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_Either, bb), bc)) → new_esEs0(xy300, xy4000, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy4000), app(ty_Maybe, bab)) → new_esEs2(xy300, xy4000, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_Maybe, bf)) → new_esEs2(xy300, xy4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(xy300), Just(xy4000), app(app(ty_@2, hh), baa)) → new_esEs1(xy300, xy4000, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy4000), app(ty_[], he)) → new_esEs(xy300, xy4000, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_@2, bd), be)) → new_esEs1(xy300, xy4000, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xy301, xy4001, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(app(ty_@3, fh), ga), gb), fa) → new_esEs3(xy300, xy4000, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(app(ty_@3, bea), beb), bec)) → new_esEs3(xy302, xy4002, bea, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(app(ty_@3, bch), bda), bdb), bah) → new_esEs3(xy301, xy4001, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bbf), bbg), bbh), bag, bah) → new_esEs3(xy300, xy4000, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Left(xy300), Left(xy4000), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xy300, xy4000, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(xy300), Right(xy4000), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xy300, xy4000, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_Either, fb), fc), fa) → new_esEs0(xy300, xy4000, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_Either, ge), gf)) → new_esEs0(xy301, xy4001, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_Maybe, fg), fa) → new_esEs2(xy300, xy4000, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_Maybe, ha)) → new_esEs2(xy301, xy4001, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_@2, gg), gh)) → new_esEs1(xy301, xy4001, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_@2, fd), ff), fa) → new_esEs1(xy300, xy4000, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_[], gd)) → new_esEs(xy301, xy4001, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_[], eh), fa) → new_esEs(xy300, xy4000, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), cb) → new_esEs(xy301, xy4001, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_[], ba)) → new_esEs(xy300, xy4000, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(ty_Either, bcc), bcd), bah) → new_esEs0(xy301, xy4001, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(ty_Either, bdd), bde)) → new_esEs0(xy302, xy4002, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bba), bbb), bag, bah) → new_esEs0(xy300, xy4000, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(app(ty_Either, ce), cf), cd) → new_esEs0(xy300, xy4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xy300), Right(xy4000), df, app(app(ty_Either, dh), ea)) → new_esEs0(xy300, xy4000, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(ty_Maybe, bcg), bah) → new_esEs2(xy301, xy4001, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(ty_Maybe, bdh)) → new_esEs2(xy302, xy4002, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bbe), bag, bah) → new_esEs2(xy300, xy4000, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Left(xy300), Left(xy4000), app(ty_Maybe, db), cd) → new_esEs2(xy300, xy4000, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy300), Right(xy4000), df, app(ty_Maybe, ed)) → new_esEs2(xy300, xy4000, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(app(ty_@2, bce), bcf), bah) → new_esEs1(xy301, xy4001, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bbc), bbd), bag, bah) → new_esEs1(xy300, xy4000, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(app(ty_@2, bdf), bdg)) → new_esEs1(xy302, xy4002, bdf, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, bag, app(ty_[], bdc)) → new_esEs(xy302, xy4002, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_[], baf), bag, bah) → new_esEs(xy300, xy4000, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bca, app(ty_[], bcb), bah) → new_esEs(xy301, xy4001, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Right(xy300), Right(xy4000), df, app(app(ty_@2, eb), ec)) → new_esEs1(xy300, xy4000, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(app(ty_@2, cg), da), cd) → new_esEs1(xy300, xy4000, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(ty_[], cc), cd) → new_esEs(xy300, xy4000, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy300), Right(xy4000), df, app(ty_[], dg)) → new_esEs(xy300, xy4000, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(Nothing, :(Just(xy400), xy41), ba) → new_deleteBy(Nothing, xy41, ba)
new_deleteBy(Just(xy30), :(Nothing, xy41), ba) → new_deleteBy(Just(xy30), xy41, ba)
new_deleteBy(Just(xy30), :(Just(xy400), xy41), ba) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, ba), ba)
new_deleteBy0(xy10, xy11, xy12, False, bb) → new_deleteBy(Just(xy12), xy10, bb)
The TRS R consists of the following rules:
new_esEs9(xy302, xy4002, app(ty_Maybe, eh)) → new_esEs17(xy302, xy4002, eh)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs14(xy30, xy400)
new_esEs26(xy301, xy4001, app(app(ty_@2, bbd), bbe)) → new_esEs12(xy301, xy4001, bbd, bbe)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs7(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs15(xy30, xy400)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bc), bd), be)) → new_esEs6(xy30, xy400, bc, bd, be)
new_esEs9(xy302, xy4002, app(ty_[], ec)) → new_esEs10(xy302, xy4002, ec)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_Either, ed), ee)) → new_esEs11(xy302, xy4002, ed, ee)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs15(EQ, EQ) → True
new_esEs25(xy300, xy4000, app(ty_Maybe, bad)) → new_esEs17(xy300, xy4000, bad)
new_esEs24(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs17(xy300, xy4000, hb)
new_esEs7(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_@2, bdh), bea)) → new_esEs12(xy300, xy4000, bdh, bea)
new_esEs8(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_Either, fg), fh)) → new_esEs11(xy30, xy400, fg, fh)
new_esEs17(Just(xy300), Just(xy4000), ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_@2, bfb), bfc)) → new_esEs12(xy300, xy4000, bfb, bfc)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs5(xy302, xy4002)
new_primMulNat0(Zero, Zero) → Zero
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Char) → new_esEs5(xy30, xy400)
new_esEs8(xy301, xy4001, app(app(app(ty_@3, dh), ea), eb)) → new_esEs6(xy301, xy4001, dh, ea, eb)
new_esEs4(xy30, xy400, app(ty_Ratio, gd)) → new_esEs18(xy30, xy400, gd)
new_esEs11(Left(xy300), Left(xy4000), app(ty_[], bcc), fh) → new_esEs10(xy300, xy4000, bcc)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_[], bde)) → new_esEs10(xy300, xy4000, bde)
new_esEs26(xy301, xy4001, app(ty_Ratio, bbg)) → new_esEs18(xy301, xy4001, bbg)
new_esEs25(xy300, xy4000, app(ty_Ratio, bae)) → new_esEs18(xy300, xy4000, bae)
new_esEs24(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs8(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs16(xy302, xy4002)
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs11(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), fh) → new_esEs6(xy300, xy4000, bdb, bdc, bdd)
new_esEs8(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_[], bba)) → new_esEs10(xy301, xy4001, bba)
new_esEs24(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_Either, bdf), bdg)) → new_esEs11(xy300, xy4000, bdf, bdg)
new_esEs7(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Float) → new_esEs21(xy30, xy400)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Maybe, beb)) → new_esEs17(xy300, xy4000, beb)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Ratio, bda), fh) → new_esEs18(xy300, xy4000, bda)
new_esEs9(xy302, xy4002, app(ty_Ratio, fa)) → new_esEs18(xy302, xy4002, fa)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs13(xy302, xy4002)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs13(xy30, xy400)
new_esEs17(Just(xy300), Just(xy4000), app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs6(xy300, xy4000, bff, bfg, bfh)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs15(xy302, xy4002)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), fh) → new_esEs11(xy300, xy4000, bcd, bce)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(app(ty_@3, bed), bee), bef)) → new_esEs6(xy300, xy4000, bed, bee, bef)
new_esEs4(xy30, xy400, app(ty_Maybe, gc)) → new_esEs17(xy30, xy400, gc)
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Succ(xy3000), Zero) → False
new_esEs21(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs11(Left(xy300), Left(xy4000), ty_Char, fh) → new_esEs5(xy300, xy4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs11(Left(xy300), Left(xy4000), ty_Double, fh) → new_esEs20(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Int, fh) → new_esEs16(xy300, xy4000)
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs25(xy300, xy4000, app(ty_[], hg)) → new_esEs10(xy300, xy4000, hg)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs17(Just(xy300), Just(xy4000), ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_Either, bbb), bbc)) → new_esEs11(xy301, xy4001, bbb, bbc)
new_esEs15(LT, LT) → True
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_[], ff)) → new_esEs10(xy30, xy400, ff)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs14(xy302, xy4002)
new_esEs24(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Char) → new_esEs5(xy300, xy4000)
new_primPlusNat1(Succ(xy200), xy400100) → Succ(Succ(new_primPlusNat0(xy200, xy400100)))
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs9(xy302, xy4002, ty_Double) → new_esEs20(xy302, xy4002)
new_esEs20(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs7(xy300, xy4000, app(app(ty_@2, ca), cb)) → new_esEs12(xy300, xy4000, ca, cb)
new_esEs11(Left(xy300), Left(xy4000), ty_Bool, fh) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), fh) → new_esEs12(xy300, xy4000, bcf, bcg)
new_esEs8(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs5(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs24(xy300, xy4000, app(ty_[], ge)) → new_esEs10(xy300, xy4000, ge)
new_esEs17(Just(xy300), Just(xy4000), ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Ratio, bfe)) → new_esEs18(xy300, xy4000, bfe)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_esEs17(Just(xy300), Just(xy4000), ty_Double) → new_esEs20(xy300, xy4000)
new_esEs10(:(xy300, xy301), :(xy4000, xy4001), ff) → new_asAs(new_esEs24(xy300, xy4000, ff), new_esEs10(xy301, xy4001, ff))
new_esEs11(Left(xy300), Left(xy4000), ty_@0, fh) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs24(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs12(xy300, xy4000, gh, ha)
new_esEs8(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs7(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_asAs(False, xy19) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs6(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bc, bd, be) → new_asAs(new_esEs7(xy300, xy4000, bc), new_asAs(new_esEs8(xy301, xy4001, bd), new_esEs9(xy302, xy4002, be)))
new_primEqNat0(Zero, Zero) → True
new_esEs24(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, bab), bac)) → new_esEs12(xy300, xy4000, bab, bac)
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_esEs4(xy30, xy400, ty_@0) → new_esEs19(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat1(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs17(Just(xy300), Just(xy4000), ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs16(xy30, xy400)
new_esEs24(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_Either, beh), bfa)) → new_esEs11(xy300, xy4000, beh, bfa)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, bbf)) → new_esEs17(xy301, xy4001, bbf)
new_esEs11(Left(xy300), Left(xy4000), ty_Float, fh) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, baf), bag), bah)) → new_esEs6(xy300, xy4000, baf, bag, bah)
new_esEs8(xy301, xy4001, app(ty_Ratio, dg)) → new_esEs18(xy301, xy4001, dg)
new_esEs8(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs17(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_@2, ef), eg)) → new_esEs12(xy302, xy4002, ef, eg)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs14(True, True) → True
new_esEs11(Left(xy300), Left(xy4000), ty_Ordering, fh) → new_esEs15(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs6(xy301, xy4001, bbh, bca, bcb)
new_esEs13(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs8(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Maybe, bch), fh) → new_esEs17(xy300, xy4000, bch)
new_esEs7(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs12(@2(xy300, xy301), @2(xy4000, xy4001), ga, gb) → new_asAs(new_esEs25(xy300, xy4000, ga), new_esEs26(xy301, xy4001, gb))
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs18(:%(xy300, xy301), :%(xy4000, xy4001), gd) → new_asAs(new_esEs22(xy300, xy4000, gd), new_esEs23(xy301, xy4001, gd))
new_esEs24(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs20(xy30, xy400)
new_esEs16(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs21(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(ty_@2, ga), gb)) → new_esEs12(xy30, xy400, ga, gb)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs7(xy300, xy4000, app(ty_[], bf)) → new_esEs10(xy300, xy4000, bf)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs19(xy302, xy4002)
new_esEs24(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs6(xy300, xy4000, hd, he, hf)
new_esEs14(False, False) → True
new_esEs8(xy301, xy4001, app(app(ty_@2, dd), de)) → new_esEs12(xy301, xy4001, dd, de)
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, gc) → True
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Ratio, bec)) → new_esEs18(xy300, xy4000, bec)
new_esEs8(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_primPlusNat1(Zero, xy400100) → Succ(xy400100)
new_esEs8(xy301, xy4001, app(app(ty_Either, db), dc)) → new_esEs11(xy301, xy4001, db, dc)
new_primPlusNat0(Succ(xy2000), Succ(xy4001000)) → Succ(Succ(new_primPlusNat0(xy2000, xy4001000)))
new_esEs25(xy300, xy4000, app(app(ty_Either, hh), baa)) → new_esEs11(xy300, xy4000, hh, baa)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, fb), fc), fd)) → new_esEs6(xy302, xy4002, fb, fc, fd)
new_esEs7(xy300, xy4000, app(ty_Maybe, cc)) → new_esEs17(xy300, xy4000, cc)
new_esEs19(@0, @0) → True
new_asAs(True, xy19) → xy19
new_esEs10(:(xy300, xy301), [], ff) → False
new_esEs10([], :(xy4000, xy4001), ff) → False
new_esEs17(Just(xy300), Just(xy4000), app(ty_[], beg)) → new_esEs10(xy300, xy4000, beg)
new_esEs17(Just(xy300), Just(xy4000), ty_Int) → new_esEs16(xy300, xy4000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs24(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs14(False, True) → False
new_esEs14(True, False) → False
new_esEs17(Just(xy300), Nothing, gc) → False
new_esEs17(Nothing, Just(xy4000), gc) → False
new_esEs7(xy300, xy4000, app(app(ty_Either, bg), bh)) → new_esEs11(xy300, xy4000, bg, bh)
new_esEs10([], [], ff) → True
new_esEs17(Just(xy300), Just(xy4000), ty_Float) → new_esEs21(xy300, xy4000)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs15(GT, GT) → True
new_esEs24(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs18(xy300, xy4000, hc)
new_esEs7(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs7(xy300, xy4000, app(ty_Ratio, cd)) → new_esEs18(xy300, xy4000, cd)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Maybe, bfd)) → new_esEs17(xy300, xy4000, bfd)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs8(xy301, xy4001, app(ty_[], da)) → new_esEs10(xy301, xy4001, da)
new_esEs24(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs11(xy300, xy4000, gf, gg)
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs7(xy300, xy4000, app(app(app(ty_@3, ce), cf), cg)) → new_esEs6(xy300, xy4000, ce, cf, cg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Succ(xy2000), Zero) → Succ(xy2000)
new_primPlusNat0(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_esEs8(xy301, xy4001, app(ty_Maybe, df)) → new_esEs17(xy301, xy4001, df)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Integer, fh) → new_esEs13(xy300, xy4000)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs11(Right(xy300), Left(xy4000), fg, fh) → False
new_esEs11(Left(xy300), Right(xy4000), fg, fh) → False
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs8(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Double)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Integer)
new_esEs14(True, False)
new_esEs14(False, True)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs7(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs20(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, ty_Int)
new_esEs16(x0, x1)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs25(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs15(GT, GT)
new_esEs7(x0, x1, ty_Float)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs7(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(EQ, EQ)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(:(x0, x1), [], x2)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs10([], [], x0)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat1(Succ(x0), x1)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat1(Zero, x0)
new_esEs19(@0, @0)
new_esEs15(LT, LT)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs17(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(Nothing, :(Just(xy400), xy41), ba) → new_deleteBy(Nothing, xy41, ba)
The TRS R consists of the following rules:
new_esEs9(xy302, xy4002, app(ty_Maybe, eh)) → new_esEs17(xy302, xy4002, eh)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs14(xy30, xy400)
new_esEs26(xy301, xy4001, app(app(ty_@2, bbd), bbe)) → new_esEs12(xy301, xy4001, bbd, bbe)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs7(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs15(xy30, xy400)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bc), bd), be)) → new_esEs6(xy30, xy400, bc, bd, be)
new_esEs9(xy302, xy4002, app(ty_[], ec)) → new_esEs10(xy302, xy4002, ec)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_Either, ed), ee)) → new_esEs11(xy302, xy4002, ed, ee)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs15(EQ, EQ) → True
new_esEs25(xy300, xy4000, app(ty_Maybe, bad)) → new_esEs17(xy300, xy4000, bad)
new_esEs24(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs17(xy300, xy4000, hb)
new_esEs7(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_@2, bdh), bea)) → new_esEs12(xy300, xy4000, bdh, bea)
new_esEs8(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_Either, fg), fh)) → new_esEs11(xy30, xy400, fg, fh)
new_esEs17(Just(xy300), Just(xy4000), ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_@2, bfb), bfc)) → new_esEs12(xy300, xy4000, bfb, bfc)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs5(xy302, xy4002)
new_primMulNat0(Zero, Zero) → Zero
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Char) → new_esEs5(xy30, xy400)
new_esEs8(xy301, xy4001, app(app(app(ty_@3, dh), ea), eb)) → new_esEs6(xy301, xy4001, dh, ea, eb)
new_esEs4(xy30, xy400, app(ty_Ratio, gd)) → new_esEs18(xy30, xy400, gd)
new_esEs11(Left(xy300), Left(xy4000), app(ty_[], bcc), fh) → new_esEs10(xy300, xy4000, bcc)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_[], bde)) → new_esEs10(xy300, xy4000, bde)
new_esEs26(xy301, xy4001, app(ty_Ratio, bbg)) → new_esEs18(xy301, xy4001, bbg)
new_esEs25(xy300, xy4000, app(ty_Ratio, bae)) → new_esEs18(xy300, xy4000, bae)
new_esEs24(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs8(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs16(xy302, xy4002)
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs11(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), fh) → new_esEs6(xy300, xy4000, bdb, bdc, bdd)
new_esEs8(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_[], bba)) → new_esEs10(xy301, xy4001, bba)
new_esEs24(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_Either, bdf), bdg)) → new_esEs11(xy300, xy4000, bdf, bdg)
new_esEs7(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Float) → new_esEs21(xy30, xy400)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Maybe, beb)) → new_esEs17(xy300, xy4000, beb)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Ratio, bda), fh) → new_esEs18(xy300, xy4000, bda)
new_esEs9(xy302, xy4002, app(ty_Ratio, fa)) → new_esEs18(xy302, xy4002, fa)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs13(xy302, xy4002)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs13(xy30, xy400)
new_esEs17(Just(xy300), Just(xy4000), app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs6(xy300, xy4000, bff, bfg, bfh)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs15(xy302, xy4002)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), fh) → new_esEs11(xy300, xy4000, bcd, bce)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(app(ty_@3, bed), bee), bef)) → new_esEs6(xy300, xy4000, bed, bee, bef)
new_esEs4(xy30, xy400, app(ty_Maybe, gc)) → new_esEs17(xy30, xy400, gc)
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Succ(xy3000), Zero) → False
new_esEs21(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs11(Left(xy300), Left(xy4000), ty_Char, fh) → new_esEs5(xy300, xy4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs11(Left(xy300), Left(xy4000), ty_Double, fh) → new_esEs20(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Int, fh) → new_esEs16(xy300, xy4000)
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs25(xy300, xy4000, app(ty_[], hg)) → new_esEs10(xy300, xy4000, hg)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs17(Just(xy300), Just(xy4000), ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_Either, bbb), bbc)) → new_esEs11(xy301, xy4001, bbb, bbc)
new_esEs15(LT, LT) → True
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_[], ff)) → new_esEs10(xy30, xy400, ff)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs14(xy302, xy4002)
new_esEs24(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Char) → new_esEs5(xy300, xy4000)
new_primPlusNat1(Succ(xy200), xy400100) → Succ(Succ(new_primPlusNat0(xy200, xy400100)))
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs9(xy302, xy4002, ty_Double) → new_esEs20(xy302, xy4002)
new_esEs20(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs7(xy300, xy4000, app(app(ty_@2, ca), cb)) → new_esEs12(xy300, xy4000, ca, cb)
new_esEs11(Left(xy300), Left(xy4000), ty_Bool, fh) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), fh) → new_esEs12(xy300, xy4000, bcf, bcg)
new_esEs8(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs5(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs24(xy300, xy4000, app(ty_[], ge)) → new_esEs10(xy300, xy4000, ge)
new_esEs17(Just(xy300), Just(xy4000), ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Ratio, bfe)) → new_esEs18(xy300, xy4000, bfe)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_esEs17(Just(xy300), Just(xy4000), ty_Double) → new_esEs20(xy300, xy4000)
new_esEs10(:(xy300, xy301), :(xy4000, xy4001), ff) → new_asAs(new_esEs24(xy300, xy4000, ff), new_esEs10(xy301, xy4001, ff))
new_esEs11(Left(xy300), Left(xy4000), ty_@0, fh) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs24(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs12(xy300, xy4000, gh, ha)
new_esEs8(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs7(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_asAs(False, xy19) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs6(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bc, bd, be) → new_asAs(new_esEs7(xy300, xy4000, bc), new_asAs(new_esEs8(xy301, xy4001, bd), new_esEs9(xy302, xy4002, be)))
new_primEqNat0(Zero, Zero) → True
new_esEs24(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, bab), bac)) → new_esEs12(xy300, xy4000, bab, bac)
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_esEs4(xy30, xy400, ty_@0) → new_esEs19(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat1(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs17(Just(xy300), Just(xy4000), ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs16(xy30, xy400)
new_esEs24(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_Either, beh), bfa)) → new_esEs11(xy300, xy4000, beh, bfa)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, bbf)) → new_esEs17(xy301, xy4001, bbf)
new_esEs11(Left(xy300), Left(xy4000), ty_Float, fh) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, baf), bag), bah)) → new_esEs6(xy300, xy4000, baf, bag, bah)
new_esEs8(xy301, xy4001, app(ty_Ratio, dg)) → new_esEs18(xy301, xy4001, dg)
new_esEs8(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs17(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_@2, ef), eg)) → new_esEs12(xy302, xy4002, ef, eg)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs14(True, True) → True
new_esEs11(Left(xy300), Left(xy4000), ty_Ordering, fh) → new_esEs15(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs6(xy301, xy4001, bbh, bca, bcb)
new_esEs13(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs8(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Maybe, bch), fh) → new_esEs17(xy300, xy4000, bch)
new_esEs7(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs12(@2(xy300, xy301), @2(xy4000, xy4001), ga, gb) → new_asAs(new_esEs25(xy300, xy4000, ga), new_esEs26(xy301, xy4001, gb))
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs18(:%(xy300, xy301), :%(xy4000, xy4001), gd) → new_asAs(new_esEs22(xy300, xy4000, gd), new_esEs23(xy301, xy4001, gd))
new_esEs24(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs20(xy30, xy400)
new_esEs16(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs21(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(ty_@2, ga), gb)) → new_esEs12(xy30, xy400, ga, gb)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs7(xy300, xy4000, app(ty_[], bf)) → new_esEs10(xy300, xy4000, bf)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs19(xy302, xy4002)
new_esEs24(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs6(xy300, xy4000, hd, he, hf)
new_esEs14(False, False) → True
new_esEs8(xy301, xy4001, app(app(ty_@2, dd), de)) → new_esEs12(xy301, xy4001, dd, de)
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, gc) → True
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Ratio, bec)) → new_esEs18(xy300, xy4000, bec)
new_esEs8(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_primPlusNat1(Zero, xy400100) → Succ(xy400100)
new_esEs8(xy301, xy4001, app(app(ty_Either, db), dc)) → new_esEs11(xy301, xy4001, db, dc)
new_primPlusNat0(Succ(xy2000), Succ(xy4001000)) → Succ(Succ(new_primPlusNat0(xy2000, xy4001000)))
new_esEs25(xy300, xy4000, app(app(ty_Either, hh), baa)) → new_esEs11(xy300, xy4000, hh, baa)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, fb), fc), fd)) → new_esEs6(xy302, xy4002, fb, fc, fd)
new_esEs7(xy300, xy4000, app(ty_Maybe, cc)) → new_esEs17(xy300, xy4000, cc)
new_esEs19(@0, @0) → True
new_asAs(True, xy19) → xy19
new_esEs10(:(xy300, xy301), [], ff) → False
new_esEs10([], :(xy4000, xy4001), ff) → False
new_esEs17(Just(xy300), Just(xy4000), app(ty_[], beg)) → new_esEs10(xy300, xy4000, beg)
new_esEs17(Just(xy300), Just(xy4000), ty_Int) → new_esEs16(xy300, xy4000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs24(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs14(False, True) → False
new_esEs14(True, False) → False
new_esEs17(Just(xy300), Nothing, gc) → False
new_esEs17(Nothing, Just(xy4000), gc) → False
new_esEs7(xy300, xy4000, app(app(ty_Either, bg), bh)) → new_esEs11(xy300, xy4000, bg, bh)
new_esEs10([], [], ff) → True
new_esEs17(Just(xy300), Just(xy4000), ty_Float) → new_esEs21(xy300, xy4000)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs15(GT, GT) → True
new_esEs24(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs18(xy300, xy4000, hc)
new_esEs7(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs7(xy300, xy4000, app(ty_Ratio, cd)) → new_esEs18(xy300, xy4000, cd)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Maybe, bfd)) → new_esEs17(xy300, xy4000, bfd)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs8(xy301, xy4001, app(ty_[], da)) → new_esEs10(xy301, xy4001, da)
new_esEs24(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs11(xy300, xy4000, gf, gg)
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs7(xy300, xy4000, app(app(app(ty_@3, ce), cf), cg)) → new_esEs6(xy300, xy4000, ce, cf, cg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Succ(xy2000), Zero) → Succ(xy2000)
new_primPlusNat0(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_esEs8(xy301, xy4001, app(ty_Maybe, df)) → new_esEs17(xy301, xy4001, df)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Integer, fh) → new_esEs13(xy300, xy4000)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs11(Right(xy300), Left(xy4000), fg, fh) → False
new_esEs11(Left(xy300), Right(xy4000), fg, fh) → False
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs8(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Double)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Integer)
new_esEs14(True, False)
new_esEs14(False, True)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs7(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs20(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, ty_Int)
new_esEs16(x0, x1)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs25(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs15(GT, GT)
new_esEs7(x0, x1, ty_Float)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs7(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(EQ, EQ)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(:(x0, x1), [], x2)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs10([], [], x0)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat1(Succ(x0), x1)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat1(Zero, x0)
new_esEs19(@0, @0)
new_esEs15(LT, LT)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs17(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(Nothing, :(Just(xy400), xy41), ba) → new_deleteBy(Nothing, xy41, ba)
R is empty.
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs8(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Double)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Integer)
new_esEs14(True, False)
new_esEs14(False, True)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs7(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs20(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, ty_Int)
new_esEs16(x0, x1)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs25(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs15(GT, GT)
new_esEs7(x0, x1, ty_Float)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs7(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(EQ, EQ)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(:(x0, x1), [], x2)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs10([], [], x0)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat1(Succ(x0), x1)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat1(Zero, x0)
new_esEs19(@0, @0)
new_esEs15(LT, LT)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs17(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primPlusNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs8(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Double)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Integer)
new_esEs14(True, False)
new_esEs14(False, True)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs7(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs20(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, ty_Int)
new_esEs16(x0, x1)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs25(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs15(GT, GT)
new_esEs7(x0, x1, ty_Float)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs7(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(EQ, EQ)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(:(x0, x1), [], x2)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs10([], [], x0)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat1(Succ(x0), x1)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat1(Zero, x0)
new_esEs19(@0, @0)
new_esEs15(LT, LT)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs17(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(Nothing, :(Just(xy400), xy41), ba) → new_deleteBy(Nothing, xy41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy(Nothing, :(Just(xy400), xy41), ba) → new_deleteBy(Nothing, xy41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(Just(xy30), :(Nothing, xy41), ba) → new_deleteBy(Just(xy30), xy41, ba)
new_deleteBy(Just(xy30), :(Just(xy400), xy41), ba) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, ba), ba)
new_deleteBy0(xy10, xy11, xy12, False, bb) → new_deleteBy(Just(xy12), xy10, bb)
The TRS R consists of the following rules:
new_esEs9(xy302, xy4002, app(ty_Maybe, eh)) → new_esEs17(xy302, xy4002, eh)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs14(xy30, xy400)
new_esEs26(xy301, xy4001, app(app(ty_@2, bbd), bbe)) → new_esEs12(xy301, xy4001, bbd, bbe)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs7(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs15(xy30, xy400)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bc), bd), be)) → new_esEs6(xy30, xy400, bc, bd, be)
new_esEs9(xy302, xy4002, app(ty_[], ec)) → new_esEs10(xy302, xy4002, ec)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_Either, ed), ee)) → new_esEs11(xy302, xy4002, ed, ee)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs15(EQ, EQ) → True
new_esEs25(xy300, xy4000, app(ty_Maybe, bad)) → new_esEs17(xy300, xy4000, bad)
new_esEs24(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs17(xy300, xy4000, hb)
new_esEs7(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_@2, bdh), bea)) → new_esEs12(xy300, xy4000, bdh, bea)
new_esEs8(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_Either, fg), fh)) → new_esEs11(xy30, xy400, fg, fh)
new_esEs17(Just(xy300), Just(xy4000), ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_@2, bfb), bfc)) → new_esEs12(xy300, xy4000, bfb, bfc)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs5(xy302, xy4002)
new_primMulNat0(Zero, Zero) → Zero
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Char) → new_esEs5(xy30, xy400)
new_esEs8(xy301, xy4001, app(app(app(ty_@3, dh), ea), eb)) → new_esEs6(xy301, xy4001, dh, ea, eb)
new_esEs4(xy30, xy400, app(ty_Ratio, gd)) → new_esEs18(xy30, xy400, gd)
new_esEs11(Left(xy300), Left(xy4000), app(ty_[], bcc), fh) → new_esEs10(xy300, xy4000, bcc)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_[], bde)) → new_esEs10(xy300, xy4000, bde)
new_esEs26(xy301, xy4001, app(ty_Ratio, bbg)) → new_esEs18(xy301, xy4001, bbg)
new_esEs25(xy300, xy4000, app(ty_Ratio, bae)) → new_esEs18(xy300, xy4000, bae)
new_esEs24(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs8(xy301, xy4001, ty_Bool) → new_esEs14(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs16(xy302, xy4002)
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs11(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), fh) → new_esEs6(xy300, xy4000, bdb, bdc, bdd)
new_esEs8(xy301, xy4001, ty_Char) → new_esEs5(xy301, xy4001)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_[], bba)) → new_esEs10(xy301, xy4001, bba)
new_esEs24(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(ty_Either, bdf), bdg)) → new_esEs11(xy300, xy4000, bdf, bdg)
new_esEs7(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Float) → new_esEs21(xy30, xy400)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Maybe, beb)) → new_esEs17(xy300, xy4000, beb)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Ratio, bda), fh) → new_esEs18(xy300, xy4000, bda)
new_esEs9(xy302, xy4002, app(ty_Ratio, fa)) → new_esEs18(xy302, xy4002, fa)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs13(xy302, xy4002)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs13(xy30, xy400)
new_esEs17(Just(xy300), Just(xy4000), app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs6(xy300, xy4000, bff, bfg, bfh)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs15(xy302, xy4002)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), fh) → new_esEs11(xy300, xy4000, bcd, bce)
new_esEs11(Right(xy300), Right(xy4000), fg, app(app(app(ty_@3, bed), bee), bef)) → new_esEs6(xy300, xy4000, bed, bee, bef)
new_esEs4(xy30, xy400, app(ty_Maybe, gc)) → new_esEs17(xy30, xy400, gc)
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Succ(xy3000), Zero) → False
new_esEs21(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs11(Left(xy300), Left(xy4000), ty_Char, fh) → new_esEs5(xy300, xy4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs11(Left(xy300), Left(xy4000), ty_Double, fh) → new_esEs20(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Int, fh) → new_esEs16(xy300, xy4000)
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs25(xy300, xy4000, app(ty_[], hg)) → new_esEs10(xy300, xy4000, hg)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs17(Just(xy300), Just(xy4000), ty_@0) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_Either, bbb), bbc)) → new_esEs11(xy301, xy4001, bbb, bbc)
new_esEs15(LT, LT) → True
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_[], ff)) → new_esEs10(xy30, xy400, ff)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs14(xy302, xy4002)
new_esEs24(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Char) → new_esEs5(xy300, xy4000)
new_primPlusNat1(Succ(xy200), xy400100) → Succ(Succ(new_primPlusNat0(xy200, xy400100)))
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs9(xy302, xy4002, ty_Double) → new_esEs20(xy302, xy4002)
new_esEs20(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs16(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs7(xy300, xy4000, app(app(ty_@2, ca), cb)) → new_esEs12(xy300, xy4000, ca, cb)
new_esEs11(Left(xy300), Left(xy4000), ty_Bool, fh) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), fh) → new_esEs12(xy300, xy4000, bcf, bcg)
new_esEs8(xy301, xy4001, ty_Ordering) → new_esEs15(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs5(xy300, xy4000)
new_esEs5(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs24(xy300, xy4000, app(ty_[], ge)) → new_esEs10(xy300, xy4000, ge)
new_esEs17(Just(xy300), Just(xy4000), ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Ratio, bfe)) → new_esEs18(xy300, xy4000, bfe)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_esEs17(Just(xy300), Just(xy4000), ty_Double) → new_esEs20(xy300, xy4000)
new_esEs10(:(xy300, xy301), :(xy4000, xy4001), ff) → new_asAs(new_esEs24(xy300, xy4000, ff), new_esEs10(xy301, xy4001, ff))
new_esEs11(Left(xy300), Left(xy4000), ty_@0, fh) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs24(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs12(xy300, xy4000, gh, ha)
new_esEs8(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs7(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_asAs(False, xy19) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs6(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bc, bd, be) → new_asAs(new_esEs7(xy300, xy4000, bc), new_asAs(new_esEs8(xy301, xy4001, bd), new_esEs9(xy302, xy4002, be)))
new_primEqNat0(Zero, Zero) → True
new_esEs24(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, bab), bac)) → new_esEs12(xy300, xy4000, bab, bac)
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_esEs4(xy30, xy400, ty_@0) → new_esEs19(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs13(xy301, xy4001)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat1(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs17(Just(xy300), Just(xy4000), ty_Char) → new_esEs5(xy300, xy4000)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs16(xy30, xy400)
new_esEs24(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(app(ty_Either, beh), bfa)) → new_esEs11(xy300, xy4000, beh, bfa)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, bbf)) → new_esEs17(xy301, xy4001, bbf)
new_esEs11(Left(xy300), Left(xy4000), ty_Float, fh) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, baf), bag), bah)) → new_esEs6(xy300, xy4000, baf, bag, bah)
new_esEs8(xy301, xy4001, app(ty_Ratio, dg)) → new_esEs18(xy301, xy4001, dg)
new_esEs8(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs17(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs9(xy302, xy4002, app(app(ty_@2, ef), eg)) → new_esEs12(xy302, xy4002, ef, eg)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs16(xy301, xy4001)
new_esEs14(True, True) → True
new_esEs11(Left(xy300), Left(xy4000), ty_Ordering, fh) → new_esEs15(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs6(xy301, xy4001, bbh, bca, bcb)
new_esEs13(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs8(xy301, xy4001, ty_@0) → new_esEs19(xy301, xy4001)
new_esEs11(Left(xy300), Left(xy4000), app(ty_Maybe, bch), fh) → new_esEs17(xy300, xy4000, bch)
new_esEs7(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs12(@2(xy300, xy301), @2(xy4000, xy4001), ga, gb) → new_asAs(new_esEs25(xy300, xy4000, ga), new_esEs26(xy301, xy4001, gb))
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs18(:%(xy300, xy301), :%(xy4000, xy4001), gd) → new_asAs(new_esEs22(xy300, xy4000, gd), new_esEs23(xy301, xy4001, gd))
new_esEs24(xy300, xy4000, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs20(xy30, xy400)
new_esEs16(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs21(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs21(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(ty_@2, ga), gb)) → new_esEs12(xy30, xy400, ga, gb)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs7(xy300, xy4000, app(ty_[], bf)) → new_esEs10(xy300, xy4000, bf)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs19(xy302, xy4002)
new_esEs24(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs6(xy300, xy4000, hd, he, hf)
new_esEs14(False, False) → True
new_esEs8(xy301, xy4001, app(app(ty_@2, dd), de)) → new_esEs12(xy301, xy4001, dd, de)
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs17(Nothing, Nothing, gc) → True
new_esEs11(Right(xy300), Right(xy4000), fg, app(ty_Ratio, bec)) → new_esEs18(xy300, xy4000, bec)
new_esEs8(xy301, xy4001, ty_Double) → new_esEs20(xy301, xy4001)
new_primPlusNat1(Zero, xy400100) → Succ(xy400100)
new_esEs8(xy301, xy4001, app(app(ty_Either, db), dc)) → new_esEs11(xy301, xy4001, db, dc)
new_primPlusNat0(Succ(xy2000), Succ(xy4001000)) → Succ(Succ(new_primPlusNat0(xy2000, xy4001000)))
new_esEs25(xy300, xy4000, app(app(ty_Either, hh), baa)) → new_esEs11(xy300, xy4000, hh, baa)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, fb), fc), fd)) → new_esEs6(xy302, xy4002, fb, fc, fd)
new_esEs7(xy300, xy4000, app(ty_Maybe, cc)) → new_esEs17(xy300, xy4000, cc)
new_esEs19(@0, @0) → True
new_asAs(True, xy19) → xy19
new_esEs10(:(xy300, xy301), [], ff) → False
new_esEs10([], :(xy4000, xy4001), ff) → False
new_esEs17(Just(xy300), Just(xy4000), app(ty_[], beg)) → new_esEs10(xy300, xy4000, beg)
new_esEs17(Just(xy300), Just(xy4000), ty_Int) → new_esEs16(xy300, xy4000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs24(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs14(False, True) → False
new_esEs14(True, False) → False
new_esEs17(Just(xy300), Nothing, gc) → False
new_esEs17(Nothing, Just(xy4000), gc) → False
new_esEs7(xy300, xy4000, app(app(ty_Either, bg), bh)) → new_esEs11(xy300, xy4000, bg, bh)
new_esEs10([], [], ff) → True
new_esEs17(Just(xy300), Just(xy4000), ty_Float) → new_esEs21(xy300, xy4000)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs15(GT, GT) → True
new_esEs24(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs18(xy300, xy4000, hc)
new_esEs7(xy300, xy4000, ty_Float) → new_esEs21(xy300, xy4000)
new_esEs7(xy300, xy4000, app(ty_Ratio, cd)) → new_esEs18(xy300, xy4000, cd)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs19(xy300, xy4000)
new_esEs17(Just(xy300), Just(xy4000), app(ty_Maybe, bfd)) → new_esEs17(xy300, xy4000, bfd)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs15(xy300, xy4000)
new_esEs8(xy301, xy4001, app(ty_[], da)) → new_esEs10(xy301, xy4001, da)
new_esEs24(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs11(xy300, xy4000, gf, gg)
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs13(xy300, xy4000)
new_esEs7(xy300, xy4000, app(app(app(ty_@3, ce), cf), cg)) → new_esEs6(xy300, xy4000, ce, cf, cg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Succ(xy2000), Zero) → Succ(xy2000)
new_primPlusNat0(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_esEs8(xy301, xy4001, app(ty_Maybe, df)) → new_esEs17(xy301, xy4001, df)
new_esEs11(Right(xy300), Right(xy4000), fg, ty_Bool) → new_esEs14(xy300, xy4000)
new_esEs11(Left(xy300), Left(xy4000), ty_Integer, fh) → new_esEs13(xy300, xy4000)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs16(xy300, xy4000)
new_esEs7(xy300, xy4000, ty_Double) → new_esEs20(xy300, xy4000)
new_esEs11(Right(xy300), Left(xy4000), fg, fh) → False
new_esEs11(Left(xy300), Right(xy4000), fg, fh) → False
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_asAs(True, x0)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs8(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Double)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs11(Left(x0), Left(x1), ty_Double, x2)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Integer)
new_esEs14(True, False)
new_esEs14(False, True)
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_esEs11(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Double)
new_esEs7(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs5(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Float)
new_esEs20(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, ty_Int)
new_esEs16(x0, x1)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Bool)
new_esEs11(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs11(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs14(True, True)
new_esEs25(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Integer)
new_esEs8(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs10([], :(x0, x1), x2)
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs15(GT, GT)
new_esEs7(x0, x1, ty_Float)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs7(x0, x1, ty_Integer)
new_esEs11(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs11(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs11(Right(x0), Right(x1), x2, ty_Bool)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15(EQ, EQ)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, ty_Float)
new_esEs11(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Integer)
new_esEs11(Right(x0), Left(x1), x2, x3)
new_esEs11(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(:(x0, x1), [], x2)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(Right(x0), Right(x1), x2, ty_Char)
new_esEs10([], [], x0)
new_esEs11(Right(x0), Right(x1), x2, ty_Integer)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs7(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat0(Zero, Zero)
new_esEs11(Left(x0), Left(x1), ty_Bool, x2)
new_primPlusNat1(Succ(x0), x1)
new_esEs11(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, ty_Int)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs15(LT, EQ)
new_esEs15(EQ, LT)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs14(False, False)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs17(Just(x0), Just(x1), ty_Double)
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs8(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(Left(x0), Left(x1), ty_Int, x2)
new_primPlusNat1(Zero, x0)
new_esEs19(@0, @0)
new_esEs15(LT, LT)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs17(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_primMulNat0(Succ(x0), Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy0(xy10, xy11, xy12, False, bb) → new_deleteBy(Just(xy12), xy10, bb)
The graph contains the following edges 1 >= 2, 5 >= 3
- new_deleteBy(Just(xy30), :(Nothing, xy41), ba) → new_deleteBy(Just(xy30), xy41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
- new_deleteBy(Just(xy30), :(Just(xy400), xy41), ba) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, ba), ba)
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 3 >= 5